#!/usr/bin/env python

import os, sys, re

def usage():
  print >> sys.stderr, "Usage: " + sys.argv[0] + " [-debug|-release] bc_file removed_func ..."
  print >> sys.stderr, "Convenience: wait = pthread_barrier_wait & pthread_cond_wait"
  print >> sys.stderr, "             barrier = pthread_barrier_wait"
  print >> sys.stderr, "             mutex = pthread_mutex_lock & pthread_mutex_unlock"

DEFENS_ROOT = os.environ["DEFENS_ROOT"]
KLEE_ROOT = DEFENS_ROOT + "/rcs-modules/klee"

version = "Release"
bc_path = ""
remove_func = []

for arg in sys.argv[1:]:
  if arg == "-h":
    usage()
    sys.exit()
  elif arg == "-debug":
    version = "Debug"
  elif arg == "-release":
    version = "Release"
  else:
    if bc_path == "":
      bc_path = arg
    else:
      if arg == "wait":
        remove_func.append("pthread_cond_wait")
        remove_func.append("pthread_cond_timedwait")
      elif arg == "barrier":
        remove_func.append("pthread_barrier_wait")
      elif arg == "mutex":
        remove_func.append("pthread_mutex_lock")
        remove_func.append("pthread_mutex_unlock")
      else:
        remove_func.append(arg)

bc_dir, bc_file = os.path.split(bc_path)
if bc_file == "":
  print >> sys.stderr, bc_path + " is not a file"
  usage()
  sys.exit()
if bc_dir == "":
  bc_dir = "."

bc_name, bc_ext = os.path.splitext(bc_file)
if bc_ext != ".bc":
  print >> sys.stderr, bc_path + " is not a bc file"
  usage()
  sys.exit()

os.system("llvm-dis " + bc_path + " -o " + bc_dir + "/" + bc_name + ".ll")

if not bc_name.endswith("-replay"):
  print >> sys.stderr, bc_path + " is not a *-replay.bc file"
  usage()
  sys.exit()

rm_name = bc_name[:-7] + "-rmsync"

print >> sys.stderr, "remove " + " ".join(remove_func) + " from " + bc_path + " (version = " + version + ")"

ll_file = file(bc_dir + "/" + bc_name + ".ll", "r")
rm_ll_file = file(bc_dir + "/" + rm_name + ".ll", "w")

while True:
  line = ll_file.readline();
  if line == "":
    break

  for func in remove_func:
    if line.find("@" + func) != -1:
      sys.stderr.write(line)
      line = re.subn("=", "= sub i32 0, 0 ;", line, 1)[0]
      sys.stderr.write(line)
      sys.stderr.write("\n")

  rm_ll_file.write(line)

ll_file.close()
rm_ll_file.close()


cmd = "llvm-as " + bc_dir + "/" + rm_name + ".ll" + " -o " + bc_dir + "/" + rm_name + ".bc"
print >> sys.stderr, cmd
os.system(cmd)

cmd = "llc " + bc_dir + "/" + rm_name + ".bc" + " -o " + bc_dir + "/" + rm_name + ".s"
print >> sys.stderr, cmd
os.system(cmd)

if version == "Release":
  build_app_path = KLEE_ROOT + "/released-tern-build-app.sh"
else:
  build_app_path = KLEE_ROOT + "/tern-build-app.sh"

build_app = file(build_app_path, "r")

nextline = False
cmd = ""
while True:
  line = build_app.readline()
  if line == "":
    break

  line = line.strip()
  if nextline or line.startswith("g++"):
    if line.endswith("\\"):
      cmd = cmd + " " + line[:-1]
      nextline = True
    else:
      cmd = cmd + " " + line
      break

cmd = re.subn("\$DEFENS_ROOT", DEFENS_ROOT, cmd)[0]
cmd = re.subn("\$REPLAY_EXE", bc_dir + "/" + rm_name + "-tern", cmd)[0]
cmd = re.subn("\$REPLAY_ASM", bc_dir + "/" + rm_name + ".s", cmd)[0]
print >> sys.stderr, cmd
os.system(cmd)

cmd = "cp " + bc_path + " " + bc_dir + "/" + rm_name + "-replay.bc"
print >> sys.stderr, cmd
os.system(cmd)
